COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	verifiability and reliability of software
C00004 00003	hoare
C00005 00004	quotes
C00007 00005	The title, "verifiability and reliability of software",( as with most
C00024 00006	outline
C00028 ENDMK
C⊗;
verifiability and reliability of software

the problem
 bugs
  why
   halpern

proposed solutions
apg
knowledge-based
vcg

what is programming
  first, its not easy.
composition and specification
modification-editing
debugging tracing and breaking
verifying
compiling
running

first 5 involve using d.s. rep of prog.

on spec lang: is it efficient
1. does it waste my time

2. efficient use of storage structures.

spec lang.
 abstraction 
a.d.s.


teaching- ads as fundamental
draw diagram


what to do
 professionalism
    contract to licensing
 theory
    reasonably shallow: note rapidity
 teaching w.o. research in c.s. loses.

reliability ≠ correctness
 protection
 compare operating system, which has been proved correct and
 user programs, proved corect therefore running w.o. protection.
 its just asking for trouble.

history of results

programming lab



philosophy
  algorithm rather than function
  not math or engineering
  is math-like in many ways
    why this is good
  currently requires progmatism
hoare
scott
 wadsworth and co
a.d.s.
modularity
  clu
correctness of translators
on-line etv, raid
tw
huet
hansen
swinehart
snowdon
quotes

dijkstra: a machine's purpose is to execute our programs
traditional: puprose of program: to instruct machine

mark halpern: that tendency to err that programmers have been noticed
to share with other human beings has often been treated as if it were
an awkwardness  attendent upon  the programmer's  adolescnece,  which
like acne  would disappear  with the  craft's coming  of age.  It has
proved otherwise. 

n.  wirth:  ...programmers knowledge  must not  consist  of a  bag of
tricks and trade secretes,  but of a general intellectual  ability to
tackle  problems  systematically,   and  that  techniques  should  be
replaced (or augmented) by a method. 
The title, "verifiability and reliability of software",( as with most
titles)  is sufficiently vague  so as  to meanignless. To  be AGAINST
verifiability is  to be  against mother  and apple-pie,  or at  least
mother. 

The  general  tenor  of  this  talk  will  be  reasonably  loose  and
philosophical.  Rest assured that motherhood is safe. The main reason
for the  wishful attitude is  that the  field currently has  progress
very little from  the "wouldn't-it-be-nice" stage. Granted, there are
some quite interesting theoretical ideas which we will address in due
course. But these results  are not about to make  a tremendous impact
on everyday computing in  the near future.  So I would like to try to
take stock of the problem,  the proposed or intimated solutions,  and
try to relate that to reality. 


the problem. 

Left to their  own devices, programmers write buggy  programs. We are
not alone  in being imperfect.  Other humans have been known to err. 
What seems  strange (hindsight  is always better  than foresight)  is
that it took  so long for the programming  industry to recognize that
it was in trouble.  The first real recognition of the problem was the
NATO conference in 1968 which coined the  term " the software problem
(or crisis-- depending  on your degree of hysteria)". People had been
quite good at writing buggy programs before this, but the implication
was  that bugs  "went with  the territory".   A  few voices  had been
raised (McCarthy..).  

Why so  late? It can be argued that one of the reasons for a software
crisis is the success of  the computing industry. With more  and more
programs--  and a  sufficient enough  number of  them DID  work-- the
demand for more, better, faster also increased. The complexity of the
tasks and the projects grew.  What did NOT  grow was the set of tools
which  a  programmer  could use  to  contain  and master  complexity.
Indeed, there  have been  very few  basic changes  in the  techniques
available to a working programmer. 

assemblers, fortran, displays

I feel that there is soon to be another addition, but let me hold off
and set the stage. 

How do  you determine when a program is correct? How do you determine
when a  program meets  its specifications?    How do  you specify  or
describe a program?  Or should you? 

What are the alternatives? debugging try it until your convivced. Not
too unreasonable. Intuition and  conviction should not be  idagnored.
Indeed most mathematical proofs given in  journals relay on intuition
and conviction.  They are not fully formalized. By the way I will use
analogies  in  other  disciplines  whenever  they  seem  useful  (and
hopefully   relevant!).In  mathematics   however  we   have  a   firm
foundation:  if someone  does not  believe our  proof we  can further
formalize the reasoning,  and if taken  to extreme we can  axiomatize
the underlying theory and,  using logically valid rules of inference,
hopefully convice the  doubter of our  veracity.  Is  it too much  to
hope for that should a foundation be sought for program construction?
Again:  all  things  in  their  place;  I  do  not forsee  a  working
programmer having to give long a tedious formal proofs any  more that
i expect a good mathematician to forswear intuition for formalism. 

Dijkstra has noted  the obvious: testing can only  show that presence
of  bugs (in  a  nontrivial program),  not the  absence.So debugging,
though  very valuable,  should  not  be elevated  to  "best-possible"
without a strong effort to do better. 

Lets look at mathematics again. Whats necessary to convince a doubter
of our formal  proof? First, he  must believe the  axioms. They  must
capture a sufficient  amount of the  meat of the  intuitive argument.
(indeed the must also be consistent--frequently a non-obvious task to
verify) Second, he must  believe the rules  of inference used in  the
argument: that  they preserve  logical validity.   What's  missing in
programming?     First,  the  analogous  constructs  to  axioms,  the
convincing specification  of the  problem. Some  algorithms are  most
easily and succinctly described as themselves( shut up! he explained)
Though some can be  reduced to a  mathematical axiomaitzation, it  is
not at  all clear  that intuition  hasnt been  "had" in the  process.
Second, the analogs to mathematical rules of inference are not at all
well defined.   In  essence they  are  program transformations  which
preserve properties such that if we are "happy" about stage n we will
be "happy" about stage n+1, applying a specific transformation. 

A  significant amount of  theoretical work is going  into attempts to
clarify correctness and specification. Alas, much of it I fear misses
the mark. The  trademarks tend to be: faddy solutions, glib answers
Indeed  the field is marked with a kind of manic-depressive  attitude:
way up, then way down: mechanical translation, theorem proving now 
automatic programming and verification. A little temperance is in order.


apg and knowledge-based programming

these two areas are related--i separate them to point out a difference
in  philosophies of how things  get done. Both attempt to get the
programmer out of the loop. apg is usually more formal; typically
a non-procedural description of the programming task is expected and
a controlled search through a collection of programming techniques is
commenced attempting to implement the non-procedural with the procedural.
typical problem: many taska are just plain procedural in nature and it
is more difficult to express them non-procedurally than to just do 'em.

knowledge-based systems expect to have a model of the task environment
in mind and are able to interact with the user to come to a mutually
acceptable solution to the problem. questiona re asked, suggestions ae
ellicited. typical problem: mind reading.

verification. specify program and its no-procedural couterpart and
attempt to show consistency.

What  then are the  alternatives?   Let's move back  and look  at the
question of "what is prgramming?" First; one thing it isn't. It isn't
easy. Anyone  who thinks so  hasn't done very  much. By "not  easy" '
don't include  the usual hassles of  card punching, turn-around time,
or debugging.  I  mean the  intellectual  process of  specifying  and
implementing an algorithm: that's  difficult.  By programming then, I
mean  the process of  formulating and implementing  an algorithm. The
traditional view of programs is "a way of  instructing our machines".
I would rather  turn things around and say  the the machine's purpose
is to execute my program. 

To put it  another way: the  typical programmer's approach is  to (a)
understand  his algorithm  (b)  describe (or  code) it  in  terms the
machine  understands.    Whereas  once  the  algorithm   is  precisely
described,  the  creative juices  stop.  Note  too that  people  were
successfully writing algorithms long before computers and programming
languages were around.  One thing that  has changed is  the necessity
for  richer languages for describing  algorithms; in particular, data
structure algorithms. 

So I take an egocentric few towards machines  and programs. I want it
to  execute my presicely  specified algorithm.   Indeed even more  its
purpose is to help me  (or at least not  hinder me) in my attempt  to
develop my algorithm. I would expect to  be able to come to a machine
with  a  perhaps partially  specified  algorithm, and  have available
tools for constructing a correct realization of that algorithm.  Thus
a programming environment. 

Compare E-pub-xgp axis. 

programming environment

I will list six ingredients and discuss each a bit, but it must be emphaiszed
that none is independent. Each ingredient must be designed with all of the
other components in mind.

1. composition and specification
    spec. lang  (diagram: math→ machine → spec)
       data structures
     language definition
     power
   scott, mccarthy, hoare

2. modification and editing
     structure editing
   Interlisp, el1, huet, E, tvedit
    correctness-modification

3. debugging and tracing
     intuit, aid, runtime trace and break

4. verifying
    is it correct? vcg-hoare; boyer-moore
     
5. compiling
    

6. running

7. the forgotten phase: documentation.

Notice that in phases, 1-5 the program, or algorithm we are constructing
is being used a a data structure.

How  would  such  a  system be  used?  First  I  would  like  to  use
it--egocentricity again. More importantly i think that such a unified
approach to programming  can make  a very significant  impact on  the
quality  of programming  product.   The  best hope  is to  apply  such
techniques to the budding computer scientist.  An ititial exposure to
programming as implementation  of abstract algorithms rather  than as
exercises in coding will do much to improve the field. 

Yes, it  does require a higher  level of sophistication  than what is
normally expected  but  isn't  that  what  education  is  all  about?
Computer  scientists must  become  much  more professional  in  their
outlook.   And  as  to sophistication,  the kernel  ideas  of current
computer science are certainly less abstruse than those  of beginning
calculus.  What is  more natural  than an  algorithm--a computation--
indeed it requires much less sophistication than the understanding of
function which has had the aspects of computation abstracted out? 

Indeed the current  muddle in programming is  much of our own  doing.
For  requiring the  beginning  student to  immediately  think in  the
machine's terms  --machine  language,  and  syntax  of  pls.--we  are
telling him to stop thinking "abstractly" -- we are thus training him
to  become a  coder;  albeit a  sophisticated coder,  still  a coder.
Rather, if we say to him: if you can describe pecisely your algorithm
in terms of computational primitives, then  we will supply you with a
device for carrying out that computation. 

Compare piano and guitar--manipulative skills. 


So as an integral part of the scheme 1.-6. is a thorough revision of
computer science education and a concerted attempt at professionalism
in the field.

In essence then a proposal for a school of computation in the style
of the scools of law or medicine. 


reliability and protection. 

outline
halpern

phil  
wouldn't be nice

the problem
  bugs
  software problem-crisis 1968
  graham
  territory  mccarthy

the reason: success
  complexity
  poor tools
  the tools: assemblers, fortran, displays

what to do: correctness
  how do you specify it

alternatives: debugging
  loss, therefor correctness

analogy with math (up to a point)
 note: analogy, quotations like statistics
  proofs
  what is proof in math?
  intution
   axioms and rules

analogy in programming?

problems with analogy
  its not mathematics
  theory like garlic

theory: apg, vcg, knowledge-based
mccrthy: before prog learn, capable of being told
  manic-depressive field

alternative: prog env- interlisp
what is programming?
  what programming isn't: easy

construction of algorithms

view of machines: egocentric
 to execute my program
  i do not program to instruct the machine

programming environment
 compare e-pub-xgp axis
  is it efficient
   is incorrect program efficnet
   is repetition efficient
     key-punch

want system for professional programmer

1. construct and specify
     specification language: semantics; abstraction
       c.f. math notations.
2. modify and edit
     structure and transformations darlington
3. debug and trace
     inteprter and monitor behavior
4. verify
     for example hoare
5. compile
     note system is viable w.o. compiler
6. run

7. document(!!??!!)
     structured programming: ing

underlying this is education and professionalism: glue

current techniques: coders
  programming is either very creative or very destructive: no middle ground.

manipulative skills

school of computation like law or medicine.


efficiency.
  problems in field are conceptual, not technological

teaching: ways of thinking




   P{A}R, R∧S{B}R, R∧¬S⊃Q
_____________________________
    P{A;R while S do B}Q